While distributed systems with transfer of processes have become pervasive,methods for reasoning about their behaviour are underdeveloped. In this paperwe propose a bisimulation technique for proving behavioural equivalence of suchsystems modelled in the \emph{higher-order $\pi$-calculus with passivation}(and restriction). Previous research for this calculus is limited to contextbisimulations and normal bisimulations which are either impractical or unsound.In contrast, we provide a sound and useful definition of \emph{environmentalbisimulations}, with several non-trivial examples. Technically, a central pointin our bisimulations is the clause for parallel composition, which must accountfor passivation of the spawned processes in the middle of their execution.
展开▼
机译：尽管具有过程转移功能的分布式系统已变得很普遍，但有关其行为的推理方法却不发达。在本文中，我们提出了一种双模拟技术来证明这种系统的行为等效性，该系统以\ emph {具有钝化的高阶$ \ pi $演算}（和约束）为模型。以前对此演算的研究仅限于上下文二元模拟和不可行或不健全的普通双模拟。相反，我们提供了\ emph {environmentalbisimulations}的合理有用的定义，并提供了一些非平凡的例子。从技术上讲，我们的双仿真中的一个中心点是并行组合的子句，该子句必须在执行过程中考虑生成的进程的钝化。
展开▼
